An infinitary algebraic theory is a variant of the notion of algebraic theory that permits operations of any (infinite) arity. As a motivating example, consider the theory of suplattices, where we have, for every cardinal number , an operation to take the supremum of -many elements.
Size issues can be tricky for infinitary algebraic theories. Naïvely, one might expect there to be an infinitary algebraic theory of complete lattices too, but there is none, because a smallness condition fails. (This is connected to the nonexistence of free complete lattices.)
(To explicitly distinguish between infinitary algebraic theories and algebraic theories, we may sometimes call the former finitary.)
The notion of infinitary algebraic theory is distinguished here from the concept of -ary algebraic theory for an arity class , since these behave more similarly to finitary algebraic theories.
A many-sorted infinitary algebraic theory is a locally small category with all small products and with a small collection of objects (called sorts) such that every object is a small product of these sorts.
Given a small set , an -sorted infinitary algebraic theory is a locally small category with all small products and equipped with an -indexed family of objects (called sorts) such that every object is a small product of these sorts. (Note that an -indexed family of objects is precisely a functor to from the discrete category on .)
If is an -sorted infinitary algebraic theory, then is a many-sorted infinitary algebraic theory; conversely, any many-sorted infinitary algebraic theory may be interpreted as an -sorted infinitary algebraic theory, where is (the set of isomoprhism classes of) an appropriate family and the -indexed family is given by the identity indexing.
An unsorted infinitary algebraic theory is a locally small category with all small products and equipped with an object (so that is a pointed category) such that every object is isomorphic to for some small cardinal number . An infinitary algebraic theory is by default an unsorted infinitary algebraic theory, invoking the red herring principle. Note that an unsorted infinitary Lawvery theory is the same thing as a -sorted infinitary algebraic theory.
We will give the definitions of further special cases for unsorted infinitary algebraic theories, but these definitions may also be generalised to the many-sorted case.
Given a regular cardinal , a -ary algebraic theory is a locally small pointed category with all -ary products for such that every object is isomorphic to for some . Every -ary algebraic theory may be interpreted as an infinitary algebraic theory by using the free category with all small products on . More generally, every -ary algebraic theory may be interpreted as a -ary algebraic theory if .
A bounded infinitary algebraic theory is an infinitary algebraic theory which is (under the interpretation above) equivalent to some -ary algebraic theory.
A finitary algebraic theory is a locally small pointed category with all finitary products such that every object is isomorphic to for some natural number . A algebraic theory is by default a finitary algebraic theory, invoking the red herring principle. Note that a finitary algebraic theory is the same thing as an -ary algebraic theory.
Given a category with small products, we may be interested in knowing whether it is equivalent to a many-sorted infinitary algebraic theory (with a set of sorts). Freyd and Street (1995) have shown that a category is small if and only if both and the functor category are locally small. Analogously, it seems that a category with products may be given the structure of a many-sorted infinitary algebraic theory (with a set of sorts) if and only if both and (the category of product-preserving functors from to , a full subcategory of ) are locally small. In both cases, the ‘only if’ part is straightfoward, but we haven’t yet proved the ‘if’ part.
See the n-Forum for more preliminary results.
A multi-sorted infinitary algebraic theory defines a monadic category over Set by taking the functor category consisting of all product-preserving covariant functors from in to .
Let us write this functor category as and start by showing that it is a locally small category.
The category of product-preserving functors and natural transformations is locally small.
Let be two product-preserving covariant functors. From the definition of a multi-sorted infinitary category we see that we may choose a set of sorts, say . Let be the image of .
As is a set, the product
is a set. We define a function by sending a natural transformation to the product of its values at each . That is,
Let be an arbitrary object. From the definition of a multi-sorted infinitary algebraic theory, there is an isomorphism
for some sets . For each and , there is a projection . As and are product-preserving, we have isomorphisms
commuting with the projections. Thus for each and , we have the following commutative diagram.
Since this holds for all and , by the basic properties of products, there is a unique morphism making the diagram commute. This morphism is normally written . Thus under the isomorphism above, is taken to . As this holds for all , is completely determined by the , whence the map in (1) is injective.
Hence is a subset of a set and thus a set.
Now that we have a locally small category, the next step is to show that the forgetful functor has a left adjoint. Firstly, we need to define this forgetful functor. As we are in the most general case, the forgetful functor does not go to but to -indexed tuples of sets (or an -graded set), where is a choice of set of sorts for . To make things a little simpler, we assume that the sorting functor is injective on isomorphism classes so that if in then in . With this assumption, the forgetful functor is the evaluation functor:
The forgetful functor has a left adjoint. The left adjoint is given on objects by:
To ease the notation, let us write for the forgetful (“underlying set(s)”) functor and for the free functor.
To show the adjunction, we define the unit and counit natural transformations:
Let us consider . To define this, we evaluate it at an -graded set, , to get a morphism of graded sets, . Such a morphism is itself a natural transformation so we evaluate again at . At this point, we have a function (in )
This is simple to describe: it is assignment to of the projection onto the th -factor:
The counit, , is a little more complicated to describe. Let be a covariant product-preserving functor. Evaluated at , is a natural transformation
By the Yoneda lemma, such natural transformations are in bijective correspondence with elements of . As is product-preserving, there is a natural isomorphism:
Now for any set , there is an obvious element in : the one that has a in the th place (which corresponds to the identity function ). Taking the product of these gives an element in which we use to define .
Let us now prove that these provide the desired adjunction. For one half, we need to consider the composition:
Let us apply this to a graded set . Then we are looking at a natural transformation from
to itself. By the standard Yoneda argument, it is sufficient to look at the induced function on
and in particular at the image of the identity therein.
The first part comes from at . For each , we have a function and thus a morphism
What this does is the following: it sends component corresponding to the th projection to the th component and all other components are forgotten. Thus we have a morphism:
Under this, the identity morphism goes to the projection morphism described just above.
Now we apply to get a morphism:
To find this element, we consider the diagram:
In this diagram, we have left off the subscript on for conciseness. The vertical morphism is that induced by the projection from (2). Since we want to have this projection itself in the lower-left, an obvious place to start is with the identity in the top-left. The right-hand square commutes since the vertical maps are projections. Starting with the identity in the top-left, we get the “Yoneda element” corresponding to in the top-right. That element can be written . The vertical map selects the th element of the list and puts it in the th slot. As this is the projection , when moving back to the lower-middle, we obtain the identity morphism as required.
Now let us turn to the other half. We need to consider the composition:
So we need to start with a covariant product-preserving functor and apply . Then we are looking at a morphism of graded sets from
to itself. So we pick and look at the function
We start with the function defined by the unit :
which sends to the projection which corresponds to the th factor of the th factor.
Now we apply . This gives us a natural transformation
which we evaluate at (technically, which we evaluate at which we then evaluate at ). This natural transformation is determined by an element of and the element that we want is the image of that element under the function induced by the projection:
As is product-preserving, we can rearrange this to:
The projection selects the th term of the element in question, and this element is, by definition, . Hence the induced function on is the identity and the adjunction is shown.
Last revised on October 14, 2024 at 09:36:53. See the history of this page for a list of all contributions to it.